1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import analysis.convex.basic analysis.normed_space.bounded_linear_maps analysis.specific_limits
src └───────────────────┘ └───────────────────────────────────────┘ └──────────────────────┘
8
9 /-!
10 # Tangent cone
11
12 In this file, we define two predicates `unique_diff_within_at 𝕜 s x` and `unique_diff_on 𝕜 s`
13 ensuring that, if a function has two derivatives, then they have to coincide. As a direct
14 definition of this fact (quantifying on all target types and all functions) would depend on
15 universes, we use a more intrinsic definition: if all the possible tangent directions to the set
16 `s` at the point `x` span a dense subset of the whole subset, it is easy to check that the
17 derivative has to be unique.
18
19 Therefore, we introduce the set of all tangent directions, named `tangent_cone_at`,
20 and express `unique_diff_within_at` and `unique_diff_on` in terms of it.
21 One should however think of this definition as an implementation detail: the only reason to
22 introduce the predicates `unique_diff_within_at` and `unique_diff_on` is to ensure the uniqueness
23 of the derivative. This is why their names reflect their uses, and not how they are defined.
24
25 ## Implementation details
26
27 Note that this file is imported by `fderiv.lean`. Hence, derivatives are not defined yet. The
28 property of uniqueness of the derivative is therefore proved in `fderiv.lean`, but based on the
29 properties of the tangent cone we prove here.
30 -/
31
32 variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
33 variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
34 variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
35 variables {G : Type*} [normed_group G] [normed_space ℝ G]
id └──────────┘ └──────────┘ ┴
src └──────────┘ └──────────┘ ┴
typ └──────────┘ └──────────┘ ┴
doc └──────────┘ └──────────┘
36
37 set_option class.instance_max_depth 50
doc └──────────────────────┘
38 open filter set
39 open_locale topological_space
40
41 /-- The set of all tangent directions to the set `s` at the point `x`. -/
42 def tangent_cone_at (s : set E) (x : E) : set E :=
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
43 {y : E | ∃(c : ℕ → 𝕜) (d : ℕ → E), (∀ᶠ n in at_top, x + d n ∈ s) ∧
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ └────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └┘ └┘ └────┘┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ └────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └────┘┴
44 (tendsto (λn, ∥c n∥) at_top at_top) ∧ (tendsto (λn, c n • d n) at_top (𝓝 y))}
id └─────┘ ┴ ┴┴ ┴┴ └────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └─────┘ ┴ ┴ └────┘ └────┘ ┴ └─────┘ ┴ └────┘ ┴
typ └─────┘ ┴ ┴┴ ┴┴ └────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
doc └─────┘ └────┘ └────┘ └─────┘ └────┘ ┴
45
46 /-- A property ensuring that the tangent cone to `s` at `x` spans a dense subset of the whole space.
47 The main role of this property is to ensure that the differential within `s` at `x` is unique,
48 hence this name. The uniqueness it asserts is proved in `unique_diff_within_at.eq` in `fderiv.lean`.
49 To avoid pathologies in dimension 0, we also require that `x` belongs to the closure of `s` (which
50 is automatic when `E` is not `0`-dimensional).
51 -/
52 def unique_diff_within_at (s : set E) (x : E) : Prop :=
53 closure ((submodule.span 𝕜 (tangent_cone_at 𝕜 s x)) : set E) = univ ∧ x ∈ closure s
54
55 /-- A property ensuring that the tangent cone to `s` at any of its points spans a dense subset of
56 the whole space. The main role of this property is to ensure that the differential along `s` is
57 unique, hence this name. The uniqueness it asserts is proved in `unique_diff_on.eq` in
58 `fderiv.lean`. -/
59 def unique_diff_on (s : set E) : Prop :=
60 ∀x ∈ s, unique_diff_within_at 𝕜 s x
61
62 variables {𝕜} {x y : E} {s t : set E}
63
64 section tangent_cone
65 /- This section is devoted to the properties of the tangent cone. -/
66
67 open normed_field
68
69 lemma tangent_cone_univ : tangent_cone_at 𝕜 univ x = univ :=
70 begin
71 refine univ_subset_iff.1 (λy hy, _),
src └─────┘ └─┘ └──────┘
typ └─────┘ └─┘ └──────┘
doc └─────┘ └─┘ └──────┘
txt └─────┘ └─┘ └──────┘
par └─────┘ └─┘ └──────┘
pid ┴ └─┘ └──────┘
72 rcases exists_one_lt_norm 𝕜 with ⟨w, hw⟩,
src └─────┘ ┴ └───────────┘
typ └─────┘ ┴ └───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
73 refine ⟨λn, w^n, λn, (w^n)⁻¹ • y, univ_mem_sets' (λn, mem_univ _), _, _⟩,
src └─────┘ └─┘ └┘ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ └─────────┘
typ └─────┘ └─┘ └┘ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ └─────────┘
doc └─────┘ └─┘ └┘ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ └─────────┘
txt └─────┘ └─┘ └┘ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ └─────────┘
par └─────┘ └─┘ └┘ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ └─────────┘
pid ┴ └─┘ └┘ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ └─────────┘
74 { simp only [norm_pow],
src └─────────┘ ┴
typ └─────────┘ ┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
75 exact tendsto_pow_at_top_at_top_of_gt_1 hw },
src └────┘ ┴ ┴
typ └────┘ ┴ ┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
76 { convert tendsto_const_nhds,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
77 ext n,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
78 have : w ^ n * (w ^ n)⁻¹ = 1,
id ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴└┘
typ └─────┘ ┴ ┴ ┴┴┴ ┴┴ ┴┴┴ ┴┴└┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st └──────────────────┘└─
79 { apply mul_inv_cancel,
id └────────────┘
src └────┘└────────────┘
typ └────┘└────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└──────────────────┘└─
80 apply pow_ne_zero,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────┘└─
81 simpa [norm_eq_zero] using (ne_of_lt (lt_trans zero_lt_one hw)).symm },
id └──────────┘ └──────┘ └──────┘ └─────────┘ └┘
src └─────┘└──────────┘└──────┘ └──────┘┴ └──────┘┴└─────────┘┴ └──────┘
typ └─────┘└──────────┘└──────┘ └──────┘┴ └──────┘┴└─────────┘┴└┘└──────┘
doc └─────┘ └──────┘ ┴ ┴ ┴ └──────┘
txt └─────┘ └──────┘ ┴ ┴ ┴ └──────┘
par └─────┘ └──────┘ ┴ ┴ ┴ └──────┘
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴ └────┘└┘
st ──────────────────────────────────────────────────────────────────────────┘└┘└
82 rw [smul_smul, this, one_smul] }
id └───────┘ └──┘ └──────┘
src └──┘└───────┘└┘ └┘└──────┘└┘
typ └──┘└───────┘└┘└──┘└┘└──────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ────────────────┘└────┘└────────┘┴┴└─
83 end
st ──┘
84
85 lemma tangent_cone_mono (h : s ⊆ t) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
86 tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 t x :=
id └─────────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
87 begin
st └─────
88 rintros y ⟨c, d, ds, ctop, clim⟩,
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
txt └──────────────────────────────┘
par └──────────────────────────────┘
pid └───────────────────────┘
st ─────────────────────────────────┘└─
89 exact ⟨c, d, mem_sets_of_superset ds (λn hn, h hn), ctop, clim⟩
id ┴ ┴ └──────────────────┘ └┘ ┴ └──┘ └──┘
src └────┘ └┘ └┘└──────────────────┘┴ ┴ └────┘ ┴ └─┘ └┘ └┘
typ └────┘ ┴└┘┴└┘└──────────────────┘┴└┘┴ └────┘┴┴ └─┘└──┘└┘└──┘└┘
doc └────┘ └┘ └┘ ┴ ┴ └────┘ ┴ └─┘ └┘ └┘
txt └────┘ └┘ └┘ ┴ ┴ └────┘ ┴ └─┘ └┘ └┘
par └────┘ └┘ └┘ ┴ ┴ └────┘ ┴ └─┘ └┘ └┘
pid ┴ └┘ └┘ ┴ ┴ └────┘ ┴ └─┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────────────┘
90 end
st └─┘
91
92 /-- Auxiliary lemma ensuring that, under the assumptions defining the tangent cone,
93 the sequence `d` tends to 0 at infinity. -/
94 lemma tangent_cone_at.lim_zero {α : Type*} (l : filter α) {c : α → 𝕜} {d : α → E}
id └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴
95 (hc : tendsto (λn, ∥c n∥) l at_top) (hd : tendsto (λn, c n • d n) l (𝓝 y)) :
id └─────┘ ┴ ┴┴ ┴┴ ┴ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └────┘ └─────┘ ┴ ┴
typ └─────┘ ┴ ┴┴ ┴┴ ┴ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └────┘ └─────┘ ┴
96 tendsto d l (𝓝 0) :=
id └─────┘ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴ ┴
doc └─────┘ ┴
97 begin
st └─────
98 have A : tendsto (λn, ∥c n∥⁻¹) l (𝓝 0) := tendsto_inv_at_top_zero.comp hc,
id └─────┘ ┴┴ ┴└┘ ┴ ┴ └──────────────────────────┘ └┘
src └───────┘└─────┘┴ └─┘┴ ┴ ┴└┘└┘ ┴ ┴└─────┘└──────────────────────────┘┴
typ └───────┘└─────┘┴ └─┘┴┴┴ ┴└┘└┘┴┴ ┴└─────┘└──────────────────────────┘┴└┘
doc └───────┘└─────┘┴ └─┘ ┴ └┘ ┴ ┴└─────┘ ┴
txt └───────┘ ┴ └─┘ ┴ └┘ ┴ └─────┘ ┴
par └───────┘ ┴ └─┘ ┴ └┘ ┴ └─────┘ ┴
pid └────┘└─┘ ┴ └─┘ ┴ └┘ ┴ └─┘└──┘ ┴
st ──────────────────────────────────────────────────────────────────────────┘└─
99 have B : tendsto (λn, ∥c n • d n∥) l (𝓝 ∥y∥) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘└─────┘┴ └─┘ ┴ ┴┴┴ ┴ └┘ ┴ ┴ └────
typ └───────┘└─────┘┴ └─┘ ┴┴ ┴┴┴┴┴ └┘┴┴ ┴ ┴ └────
doc └───────┘└─────┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └────
txt └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └────
par └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └────
pid └────┘└─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└───
st ──────────────────────────────────────────────────
100 (continuous_norm.tendsto _).comp hd,
id └─────────────────────┘ └┘
src ───┘ └─────────────────────┘└───────┘
typ ───┘ └─────────────────────┘└───────┘└┘
doc ───┘ └───────┘
txt ───┘ └───────┘
par ───┘ └───────┘
pid ───┘ └───────┘
st ──────────────────────────────────────┘└─
101 have C : tendsto (λn, ∥c n∥⁻¹ * ∥c n • d n∥) l (𝓝 (0 * ∥y∥)) := A.mul B,
id └─────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
src └───────┘└─────┘┴ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └────┘└───┘┴
typ └───────┘└─────┘┴ └─┘ ┴ ┴┴┴ ┴┴ ┴ ┴┴┴ └┘┴┴ ┴ └┘ ┴ ┴ └────┘└───┘┴┴
doc └───────┘└─────┘┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └────┘ ┴
txt └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └────┘ ┴
par └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └────┘ ┴
pid └────┘└─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘└──┘ ┴
st ────────────────────────────────────────────────────────────────────────┘└─
102 rw zero_mul at C,
id └──────┘
src └─┘└──────┘└───┘
typ └─┘└──────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ─────────────────┘└─
103 have : ∀ᶠ n in l, ∥c n∥⁻¹ * ∥c n • d n∥ = ∥d n∥,
id └┘ └┘ ┴┴ ┴ ┴ ┴
src └─────┘└┘└─┘└┘┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴
typ └─────┘└┘└─┘└┘┴┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴┴
doc └─────┘└┘└─┘└┘┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────┘└─
104 { apply mem_sets_of_superset (ne_mem_of_tendsto_norm_at_top hc 0) (λn hn, _),
id └──────────────────┘ └───────────────────────────┘ └┘
src └────┘└──────────────────┘┴ └───────────────────────────┘┴ └──┘ └──────┘
typ └────┘└──────────────────┘┴ └───────────────────────────┘┴└┘└──┘ └──────┘
doc └────┘ ┴ └───────────────────────────┘┴ └──┘ └──────┘
txt └────┘ ┴ ┴ └──┘ └──────┘
par └────┘ ┴ ┴ └──┘ └──────┘
pid ┴ ┴ ┴ └──┘ └──────┘
st ───┘└─────────────────────────┘┴└────────────────────────────────────────────┘└─
105 rw [mem_set_of_eq, norm_smul, ← mul_assoc, inv_mul_cancel, one_mul],
id └───────────┘ └───────┘ └───────┘ └────────────┘ └─────┘
src └──┘└───────────┘└┘└───────┘└──┘└───────┘└┘└────────────┘└┘└─────┘┴
typ └──┘└───────────┘└┘└───────┘└──┘└───────┘└┘└────────────┘└┘└─────┘┴
doc └──┘ └┘ └──┘ └┘ └┘ ┴
txt └──┘ └┘ └──┘ └┘ └┘ ┴
par └──┘ └┘ └──┘ └┘ └┘ ┴
pid └┘ └┘ └──┘ └┘ └┘ ┴
st ────────────────────┘└─────────┘└───────────┘└──────────────┘└───────┘└──
106 rwa [ne.def, norm_eq_zero] },
id └────┘ └──────────┘
src └───┘└────┘└┘└──────────┘└┘
typ └───┘└────┘└┘└──────────┘└┘
doc └───┘ └┘ └┘
txt └───┘ └┘ └┘
par └───┘ └┘ └┘
pid └┘ └┘ ┴┴
st ──────────────┘└────────────┘┴┴└┘└
107 have D : tendsto (λ n, ∥d n∥) l (𝓝 0) :=
id └─────┘ ┴ ┴
src └───────┘└─────┘┴ └──┘ ┴ └┘ ┴ └──────
typ └───────┘└─────┘┴ └──┘ ┴┴ └┘┴┴ └──────
doc └───────┘└─────┘┴ └──┘ ┴ └┘ ┴ └──────
txt └───────┘ ┴ └──┘ ┴ └┘ ┴ └──────
par └───────┘ ┴ └──┘ ┴ └┘ ┴ └──────
pid └────┘└─┘ ┴ └──┘ ┴ └┘ ┴ └─┘└───
st ───────────────────────────────────────────
108 tendsto.congr' this C,
id └────────────┘ └──┘ ┴
src ───┘└────────────┘┴ ┴
typ ───┘└────────────┘┴└──┘┴┴
doc ───┘ ┴ ┴
txt ───┘ ┴ ┴
par ───┘ ┴ ┴
pid ───┘ ┴ ┴
st ────────────────────────┘└─
109 rw tendsto_zero_iff_norm_tendsto_zero,
id └────────────────────────────────┘
src └─┘└────────────────────────────────┘
typ └─┘└────────────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────────────────────┘└─
110 exact D
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────┘
111 end
st └─┘
112
113 lemma tangent_cone_mono_nhds (h : nhds_within x s ≤ nhds_within x t) :
id └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └─────────┘ └─────────┘
114 tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 t x :=
id └─────────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
115 begin
st └─────
116 rintros y ⟨c, d, ds, ctop, clim⟩,
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
txt └──────────────────────────────┘
par └──────────────────────────────┘
pid └───────────────────────┘
st ─────────────────────────────────┘└─
117 refine ⟨c, d, _, ctop, clim⟩,
id ┴ ┴ └──┘ └──┘
src └─────┘ └┘ └───┘ └┘ ┴
typ └─────┘ ┴└┘┴└───┘└──┘└┘└──┘┴
doc └─────┘ └┘ └───┘ └┘ ┴
txt └─────┘ └┘ └───┘ └┘ ┴
par └─────┘ └┘ └───┘ └┘ ┴
pid ┴ └┘ └───┘ └┘ ┴
st ─────────────────────────────┘└─
118 suffices : tendsto (λ n, x + d n) at_top (nhds_within x t),
id └─────┘ ┴ ┴ └────┘ └─────────┘ ┴ ┴
src └─────────┘└─────┘┴ └──┘ ┴┴┴ ┴ └┘└────┘┴ └─────────┘┴ ┴ ┴
typ └─────────┘└─────┘┴ └──┘ ┴┴┴┴┴ └┘└────┘┴ └─────────┘┴┴┴┴┴
doc └─────────┘└─────┘┴ └──┘ ┴ ┴ ┴ └┘└────┘┴ └─────────┘┴ ┴ ┴
txt └─────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └─────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └───────┘└┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────┘└─
119 from tendsto_principal.1 (tendsto_inf.1 this).2,
id └───────────────┘ └─────────┘ └──┘
src └───┘└───────────────┘└─┘ └─────────┘└─┘ └─┘
typ └───┘└───────────────┘└─┘ └─────────┘└─┘└──┘└─┘
doc └───┘ └─┘ └─┘ └─┘
txt └───┘ └─┘ └─┘ └─┘
par └───┘ └─┘ └─┘ └─┘
pid └───┘ └─┘ └─┘ ┴└┘
st ──────────────────────────────────────────────────┘└─
120 apply tendsto_le_right h,
id └──────────────┘ ┴
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────┘└─
121 refine tendsto_inf.2 ⟨_, tendsto_principal.2 ds⟩,
id └─────────┘ └───────────────┘ └┘
src └─────┘└─────────┘└─┘ └─┘└───────────────┘└─┘ ┴
typ └─────┘└─────────┘└─┘ └─┘└───────────────┘└─┘└┘┴
doc └─────┘ └─┘ └─┘ └─┘ ┴
txt └─────┘ └─┘ └─┘ └─┘ ┴
par └─────┘ └─┘ └─┘ └─┘ ┴
pid ┴ └─┘ └─┘ └─┘ ┴
st ─────────────────────────────────────────────────┘└─
122 simpa only [add_zero] using tendsto_const_nhds.add (tangent_cone_at.lim_zero at_top ctop clim)
id └──────┘ └────────────────────┘ └──────────────────────┘ └────┘ └──┘ └──┘
src └──────────┘└──────┘└──────┘└────────────────────┘┴ └──────────────────────┘┴└────┘┴ ┴ └┘
typ └──────────┘└──────┘└──────┘└────────────────────┘┴ └──────────────────────┘┴└────┘┴└──┘┴└──┘└┘
doc └──────────┘ └──────┘ ┴ └──────────────────────┘┴└────┘┴ ┴ └┘
txt └──────────┘ └──────┘ ┴ ┴ ┴ ┴ └┘
par └──────────┘ └──────┘ ┴ ┴ ┴ ┴ └┘
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘
123 end
st └─┘
124
125 /-- Tangent cone of `s` at `x` depends only on `nhds_within x s`. -/
126 lemma tangent_cone_congr (h : nhds_within x s = nhds_within x t) :
id └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └─────────┘ └─────────┘
127 tangent_cone_at 𝕜 s x = tangent_cone_at 𝕜 t x :=
id └─────────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
128 subset.antisymm
id └─────────────┘
src └─────────────┘
typ └─────────────┘
129 (tangent_cone_mono_nhds $ le_of_eq h)
id └────────────────────┘ └──────┘ ┴
src └────────────────────┘ └──────┘
typ └────────────────────┘ └──────┘ ┴
130 (tangent_cone_mono_nhds $ le_of_eq h.symm)
id └────────────────────┘ └──────┘ ┴└───┘
src └────────────────────┘ └──────┘ └───┘
typ └────────────────────┘ └──────┘ ┴└───┘
131
132 /-- Intersecting with a neighborhood of the point does not change the tangent cone. -/
133 lemma tangent_cone_inter_nhds (ht : t ∈ 𝓝 x) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
doc ┴
134 tangent_cone_at 𝕜 (s ∩ t) x = tangent_cone_at 𝕜 s x :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
135 tangent_cone_congr (nhds_within_restrict' _ ht).symm
id └────────────────┘ └───────────────────┘ └┘ └──┘
src └────────────────┘ └───────────────────┘ └──┘
typ └────────────────┘ └───────────────────┘ └┘ └──┘
doc └────────────────┘
136
137 /-- The tangent cone of a product contains the tangent cone of its left factor. -/
138 lemma subset_tangent_cone_prod_left {t : set F} {y : F} (ht : y ∈ closure t) :
id └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─┘ ┴ └─────┘
typ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
139 set.prod (tangent_cone_at 𝕜 s x) {(0 : F)} ⊆ tangent_cone_at 𝕜 (set.prod s t) (x, y) :=
id └──────┘ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
src └──────┘ └─────────────┘ ┴ ┴ └─────────────┘ └──────┘ ┴
typ └──────┘ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
doc └──────┘ └─────────────┘ └─────────────┘ └──────┘
140 begin
st └─────
141 rintros ⟨v, w⟩ ⟨⟨c, d, hd, hc, hy⟩, hw⟩,
src └─────────────────────────────────────┘
typ └─────────────────────────────────────┘
doc └─────────────────────────────────────┘
txt └─────────────────────────────────────┘
par └─────────────────────────────────────┘
pid └──────────────────────────────┘
st ────────────────────────────────────────┘└─
142 have : w = 0, by simpa using hw,
id ┴ ┴ └┘
src └─────┘ ┴┴└┘ └──────────┘
typ └─────┘┴┴┴└┘ └──────────┘└┘
doc └─────┘ ┴ └┘ └──────────┘
txt └─────┘ ┴ └┘ └──────────┘
par └─────┘ ┴ └┘ └──────────┘
pid └───┘└┘ ┴ ┴┴ ┴└────┘
st ─────────────┘ └─
143 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
144 have : ∀n, ∃d', y + d' ∈ t ∧ ∥c n • d'∥ ≤ ((1:ℝ)/2)^n,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴┴└┘┴┴ ┴┴┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴┴┴┴ └┘ ┴┴└┘┴
typ └─────┘ ┴ ┴┴└┘┴┴┴┴┴┴ ┴┴┴┴┴ ┴┴┴┴ ┴┴┴ ┴┴┴┴ └┘ ┴┴└┘┴
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
st ──────────────────────────────────────────────────────┘└─
145 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
146 have c_pos : 0 < 1 + ∥c n∥ :=
id ┴ ┴ ┴
src └─────────────┘┴└─┘ ┴ ┴ └───
typ └─────────────┘┴└─┘ ┴ ┴┴┴ └───
doc └─────────────┘ └─┘ ┴ ┴ └───
txt └─────────────┘ └─┘ ┴ ┴ └───
par └─────────────┘ └─┘ ┴ ┴ └───
pid └────────┘└───┘ └─┘ ┴ ┴ └───
st ──────────────────────────────────
147 add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _),
id └──────────────────────┘ └─────────┘ └─────────┘
src ─────┘└──────────────────────┘┴└─────────┘┴ └─────────┘└─┘
typ ─────┘└──────────────────────┘┴└─────────┘┴ └─────────┘└─┘
doc ─────┘ ┴ ┴ └─┘
txt ─────┘ ┴ ┴ └─┘
par ─────┘ ┴ ┴ └─┘
pid ─────┘ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────┘└─
148 rcases metric.mem_closure_iff'.1 ht ((1 + ∥c n∥)⁻¹ * (1/2)^n) _ with ⟨z, z_pos, hz⟩,
id └─────────────────────┘ └┘ ┴ └┘ ┴ ┴
src └─────┘└─────────────────────┘└─┘ ┴ └┘ ┴ ┴ ┴└┘┴┴┴ ┴ └┘ └─────────────────────┘
typ └─────┘└─────────────────────┘└─┘└┘┴ └┘ ┴ ┴┴ ┴└┘┴┴┴ ┴ └┘ ┴└─────────────────────┘
doc └─────┘└─────────────────────┘└─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────────────┘
txt └─────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────────────┘
par └─────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────────────┘
pid ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
149 refine ⟨z - y, _, _⟩,
id ┴ ┴ ┴
src └─────┘ ┴┴┴ └─────┘
typ └─────┘ ┴┴┴┴┴└─────┘
doc └─────┘ ┴ ┴ └─────┘
txt └─────┘ ┴ ┴ └─────┘
par └─────┘ ┴ ┴ └─────┘
pid ┴ ┴ ┴ └─────┘
st ───────────────────────┘└─
150 { convert z_pos, abel },
id └───┘
src └──────┘ └───┘
typ └──────┘└───┘ └───┘
doc └──────┘ └───┘
txt └──────┘ └───┘
par └──────┘ └───┘
pid ┴ ┴
st ─────┘└───────────┘└─────┘└┘└
151 { rw [norm_smul, ← dist_eq_norm, dist_comm],
id └───────┘ └──────────┘ └───────┘
src └──┘└───────┘└──┘└──────────┘└┘└───────┘┴
typ └──┘└───────┘└──┘└──────────┘└┘└───────┘┴
doc └──┘ └──┘ └┘ ┴
txt └──┘ └──┘ └┘ ┴
par └──┘ └──┘ └┘ ┴
pid └┘ └──┘ └┘ ┴
st ─────┘└───────────┘└──────────────┘└─────────┘└──
152 calc ∥c n∥ * dist y z ≤ (1 + ∥c n∥) * ((1 + ∥c n∥)⁻¹ * (1/2)^n) :
id └──┘ └──┘ ┴ ┴ ┴
src └──┘ └──┘
typ └──┘ └──┘ ┴ ┴ ┴
doc └──┘
st ────────────────────────────────────────────────────────────────────────
153 begin
st ─────┘└─────
154 apply mul_le_mul _ (le_of_lt hz) dist_nonneg (le_of_lt c_pos),
id └────────┘ └┘ └─────────┘ └──────┘ └───┘
src └────┘└────────┘└─┘ ┴ └┘└─────────┘┴ └──────┘┴ ┴
typ └────┘└────────┘└─┘ ┴└┘└┘└─────────┘┴ └──────┘┴└───┘┴
doc └────┘ └─┘ ┴ └┘ ┴ ┴ ┴
txt └────┘ └─┘ ┴ └┘ ┴ ┴ ┴
par └────┘ └─┘ ┴ └┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ └┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────┘└─
155 simp only [zero_le_one, le_add_iff_nonneg_left]
id └─────────┘ └────────────────────┘
src └─────────┘└─────────┘└┘└────────────────────┘└─
typ └─────────┘└─────────┘└┘└────────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st ────────────────────────────────────────────────────────
156 end
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└─┘└
157 ... = (1/2)^n :
id ┴
typ ┴
st ──────────────────────
158 begin
st ─────┘└─────
159 rw [← mul_assoc, mul_inv_cancel, one_mul],
id └───────┘ └────────────┘ └─────┘
src └────┘└───────┘└┘└────────────┘└┘└─────┘┴
typ └────┘└───────┘└┘└────────────┘└┘└─────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid └──┘ └┘ └┘ ┴
st ──────────────────────┘└──────────────┘└───────┘└──
160 exact ne_of_gt c_pos
id └──────┘ └───┘
src └────┘└──────┘┴ └
typ └────┘└──────┘┴└───┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ─────────────────────────────
161 end },
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└────┘└
162 { apply mul_pos (inv_pos c_pos) (pow_pos _ _),
id └─────┘ └─────┘ └───┘ └─────┘
src └────┘└─────┘┴ └─────┘┴ └┘ └─────┘└───┘
typ └────┘└─────┘┴ └─────┘┴└───┘└┘ └─────┘└───┘
doc └────┘ ┴ ┴ └┘ └───┘
txt └────┘ ┴ ┴ └┘ └───┘
par └────┘ ┴ ┴ └┘ └───┘
pid ┴ ┴ ┴ └┘ └───┘
st ────────────────────────────────────────────────┘└─
163 norm_num } },
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st ──────────────┘└──┘└
164 choose d' hd' using this,
id └──┘
src └──────────────────┘
typ └──────────────────┘└──┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └─┘└──┘└─────┘
st ─────────────────────────┘└─
165 refine ⟨c, λn, (d n, d' n), _, hc, _⟩,
id ┴ ┴ └┘ └┘
src └─────┘ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
typ └─────┘ ┴└┘ └─┘ ┴┴ └┘└┘┴ └────┘└┘└──┘
doc └─────┘ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
txt └─────┘ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
par └─────┘ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
pid ┴ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
st ──────────────────────────────────────┘└─
166 show ∀ᶠ n in at_top, (x, y) + (d n, d' n) ∈ set.prod s t,
id └┘ └┘ └────┘┴ ┴ ┴ ┴┴ └┘ └──────┘ ┴ ┴
src └───┘└┘└─┘└┘┴└────┘┴┴ └┘ └┘ ┴┴ ┴ └┘ ┴ └┘ ┴└──────┘┴ ┴
typ └───┘└┘└─┘└┘┴└────┘┴┴ ┴└┘┴└┘ ┴┴┴┴ └┘└┘┴ └┘ ┴└──────┘┴┴┴┴
doc └───┘└┘└─┘└┘┴└────┘┴┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴└──────┘┴ ┴
txt └───┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
par └───┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
pid └───┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
167 { apply filter.mem_sets_of_superset hd,
id └─────────────────────────┘ └┘
src └────┘└─────────────────────────┘┴
typ └────┘└─────────────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────────────────────────────────┘└─
168 assume n hn,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
169 simp at hn,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ─────────────┘└─
170 simp [hn, (hd' n).1] },
id └┘ └─┘ ┴
src └────┘ └┘ ┴ └───┘
typ └────┘└┘└┘ └─┘┴┴└───┘
doc └────┘ └┘ ┴ └───┘
txt └────┘ └┘ ┴ └───┘
par └────┘ └┘ ┴ └───┘
pid ┴┴ └┘ ┴ └──┘┴
st ────────────────────────┘└┘└
171 { apply tendsto_prod_mk_nhds hy,
id └──────────────────┘ └┘
src └────┘└──────────────────┘┴
typ └────┘└──────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────┘└─
172 change tendsto (λ (n : ℕ), c n • d' n) at_top (𝓝 0),
id └─────┘ ┴ └┘ └────┘ ┴
src └─────┘└─────┘┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘└────┘┴ ┴└─┘
typ └─────┘└─────┘┴ └────┘ └─┘┴┴ ┴ ┴└┘┴ └┘└────┘┴ ┴└─┘
doc └─────┘└─────┘┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘└────┘┴ ┴└─┘
txt └─────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
par └─────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
pid ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
st ──────────────────────────────────────────────────────┘└─
173 rw tendsto_zero_iff_norm_tendsto_zero,
id └────────────────────────────────┘
src └─┘└────────────────────────────────┘
typ └─┘└────────────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────────────────────────┘└─
174 refine squeeze_zero (λn, norm_nonneg _) (λn, (hd' n).2) _,
id └──────────┘ └─────────┘ └─┘
src └─────┘└──────────┘┴ └─┘└─────────┘└──┘ └─┘ ┴ └────┘
typ └─────┘└──────────┘┴ └─┘└─────────┘└──┘ └─┘ └─┘┴ └────┘
doc └─────┘ ┴ └─┘ └──┘ └─┘ ┴ └────┘
txt └─────┘ ┴ └─┘ └──┘ └─┘ ┴ └────┘
par └─────┘ ┴ └─┘ └──┘ └─┘ ┴ └────┘
pid ┴ ┴ └─┘ └──┘ └─┘ ┴ └────┘
st ────────────────────────────────────────────────────────────┘└─
175 apply tendsto_pow_at_top_nhds_0_of_lt_1; norm_num }
id └───────────────────────────────┘
src └────┘└───────────────────────────────┘ └───────┘
typ └────┘└───────────────────────────────┘ └───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ ┴
st ─────────────────────────────────────────────────────┘└─
176 end
st ──┘
177
178 /-- The tangent cone of a product contains the tangent cone of its right factor. -/
179 lemma subset_tangent_cone_prod_right {t : set F} {y : F}
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
180 (hs : x ∈ closure s) :
id ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ └─────┘ ┴
doc └─────┘
181 set.prod {(0 : E)} (tangent_cone_at 𝕜 t y) ⊆ tangent_cone_at 𝕜 (set.prod s t) (x, y) :=
id └──────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
src └──────┘ ┴ └─────────────┘ ┴ └─────────────┘ └──────┘ ┴
typ └──────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
doc └──────┘ └─────────────┘ └─────────────┘ └──────┘
182 begin
st └─────
183 rintros ⟨v, w⟩ ⟨hv, ⟨c, d, hd, hc, hy⟩⟩,
src └─────────────────────────────────────┘
typ └─────────────────────────────────────┘
doc └─────────────────────────────────────┘
txt └─────────────────────────────────────┘
par └─────────────────────────────────────┘
pid └──────────────────────────────┘
st ────────────────────────────────────────┘└─
184 have : v = 0, by simpa using hv,
id ┴ ┴ └┘
src └─────┘ ┴┴└┘ └──────────┘
typ └─────┘┴┴┴└┘ └──────────┘└┘
doc └─────┘ ┴ └┘ └──────────┘
txt └─────┘ ┴ └┘ └──────────┘
par └─────┘ ┴ └┘ └──────────┘
pid └───┘└┘ ┴ ┴┴ ┴└────┘
st ─────────────┘ └─
185 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
186 have : ∀n, ∃d', x + d' ∈ s ∧ ∥c n • d'∥ ≤ ((1:ℝ)/2)^n,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴┴└┘┴┴ ┴┴┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴┴┴┴ └┘ ┴┴└┘┴
typ └─────┘ ┴ ┴┴└┘┴┴┴┴┴┴ ┴┴┴┴┴ ┴┴┴┴ ┴┴┴ ┴┴┴┴ └┘ ┴┴└┘┴
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
st ──────────────────────────────────────────────────────┘└─
187 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
188 have c_pos : 0 < 1 + ∥c n∥ :=
id ┴ ┴ ┴
src └─────────────┘┴└─┘ ┴ ┴ └───
typ └─────────────┘┴└─┘ ┴ ┴┴┴ └───
doc └─────────────┘ └─┘ ┴ ┴ └───
txt └─────────────┘ └─┘ ┴ ┴ └───
par └─────────────┘ └─┘ ┴ ┴ └───
pid └────────┘└───┘ └─┘ ┴ ┴ └───
st ──────────────────────────────────
189 add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _),
id └──────────────────────┘ └─────────┘ └─────────┘
src ─────┘└──────────────────────┘┴└─────────┘┴ └─────────┘└─┘
typ ─────┘└──────────────────────┘┴└─────────┘┴ └─────────┘└─┘
doc ─────┘ ┴ ┴ └─┘
txt ─────┘ ┴ ┴ └─┘
par ─────┘ ┴ ┴ └─┘
pid ─────┘ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────┘└─
190 rcases metric.mem_closure_iff'.1 hs ((1 + ∥c n∥)⁻¹ * (1/2)^n) _ with ⟨z, z_pos, hz⟩,
id └─────────────────────┘ └┘ ┴ └┘ ┴ ┴
src └─────┘└─────────────────────┘└─┘ ┴ └┘ ┴ ┴ ┴└┘┴┴┴ ┴ └┘ └─────────────────────┘
typ └─────┘└─────────────────────┘└─┘└┘┴ └┘ ┴ ┴┴ ┴└┘┴┴┴ ┴ └┘ ┴└─────────────────────┘
doc └─────┘└─────────────────────┘└─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────────────┘
txt └─────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────────────┘
par └─────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────────────┘
pid ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
191 refine ⟨z - x, _, _⟩,
id ┴ ┴ ┴
src └─────┘ ┴┴┴ └─────┘
typ └─────┘ ┴┴┴┴┴└─────┘
doc └─────┘ ┴ ┴ └─────┘
txt └─────┘ ┴ ┴ └─────┘
par └─────┘ ┴ ┴ └─────┘
pid ┴ ┴ ┴ └─────┘
st ───────────────────────┘└─
192 { convert z_pos, abel },
id └───┘
src └──────┘ └───┘
typ └──────┘└───┘ └───┘
doc └──────┘ └───┘
txt └──────┘ └───┘
par └──────┘ └───┘
pid ┴ ┴
st ─────┘└───────────┘└─────┘└┘└
193 { rw [norm_smul, ← dist_eq_norm, dist_comm],
id └───────┘ └──────────┘ └───────┘
src └──┘└───────┘└──┘└──────────┘└┘└───────┘┴
typ └──┘└───────┘└──┘└──────────┘└┘└───────┘┴
doc └──┘ └──┘ └┘ ┴
txt └──┘ └──┘ └┘ ┴
par └──┘ └──┘ └┘ ┴
pid └┘ └──┘ └┘ ┴
st ─────┘└───────────┘└──────────────┘└─────────┘└──
194 calc ∥c n∥ * dist x z ≤ (1 + ∥c n∥) * ((1 + ∥c n∥)⁻¹ * (1/2)^n) :
id └──┘ └──┘ ┴ ┴ ┴
src └──┘ └──┘
typ └──┘ └──┘ ┴ ┴ ┴
doc └──┘
st ────────────────────────────────────────────────────────────────────────
195 begin
st ─────┘└─────
196 apply mul_le_mul _ (le_of_lt hz) dist_nonneg (le_of_lt c_pos),
id └────────┘ └┘ └─────────┘ └──────┘ └───┘
src └────┘└────────┘└─┘ ┴ └┘└─────────┘┴ └──────┘┴ ┴
typ └────┘└────────┘└─┘ ┴└┘└┘└─────────┘┴ └──────┘┴└───┘┴
doc └────┘ └─┘ ┴ └┘ ┴ ┴ ┴
txt └────┘ └─┘ ┴ └┘ ┴ ┴ ┴
par └────┘ └─┘ ┴ └┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ └┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────┘└─
197 simp only [zero_le_one, le_add_iff_nonneg_left]
id └─────────┘ └────────────────────┘
src └─────────┘└─────────┘└┘└────────────────────┘└─
typ └─────────┘└─────────┘└┘└────────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st ────────────────────────────────────────────────────────
198 end
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└─┘└
199 ... = (1/2)^n :
id ┴
typ ┴
st ──────────────────────
200 begin
st ─────┘└─────
201 rw [← mul_assoc, mul_inv_cancel, one_mul],
id └───────┘ └────────────┘ └─────┘
src └────┘└───────┘└┘└────────────┘└┘└─────┘┴
typ └────┘└───────┘└┘└────────────┘└┘└─────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid └──┘ └┘ └┘ ┴
st ──────────────────────┘└──────────────┘└───────┘└──
202 exact ne_of_gt c_pos
id └──────┘ └───┘
src └────┘└──────┘┴ └
typ └────┘└──────┘┴└───┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ─────────────────────────────
203 end },
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└────┘└
204 { apply mul_pos (inv_pos c_pos) (pow_pos _ _),
id └─────┘ └─────┘ └───┘ └─────┘
src └────┘└─────┘┴ └─────┘┴ └┘ └─────┘└───┘
typ └────┘└─────┘┴ └─────┘┴└───┘└┘ └─────┘└───┘
doc └────┘ ┴ ┴ └┘ └───┘
txt └────┘ ┴ ┴ └┘ └───┘
par └────┘ ┴ ┴ └┘ └───┘
pid ┴ ┴ ┴ └┘ └───┘
st ────────────────────────────────────────────────┘└─
205 norm_num } },
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st ──────────────┘└──┘└
206 choose d' hd' using this,
id └──┘
src └──────────────────┘
typ └──────────────────┘└──┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └─┘└──┘└─────┘
st ─────────────────────────┘└─
207 refine ⟨c, λn, (d' n, d n), _, hc, _⟩,
id ┴ └┘ ┴ └┘
src └─────┘ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
typ └─────┘ ┴└┘ └─┘ └┘┴ └┘┴┴ └────┘└┘└──┘
doc └─────┘ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
txt └─────┘ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
par └─────┘ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
pid ┴ └┘ └─┘ ┴ └┘ ┴ └────┘ └──┘
st ──────────────────────────────────────┘└─
208 show ∀ᶠ n in at_top, (x, y) + (d' n, d n) ∈ set.prod s t,
id └┘ └┘ └────┘┴ ┴ ┴ ┴└┘ ┴ └──────┘ ┴ ┴
src └───┘└┘└─┘└┘┴└────┘┴┴ └┘ └┘ ┴┴ ┴ └┘ ┴ └┘ ┴└──────┘┴ ┴
typ └───┘└┘└─┘└┘┴└────┘┴┴ ┴└┘┴└┘ ┴┴└┘┴ └┘┴┴ └┘ ┴└──────┘┴┴┴┴
doc └───┘└┘└─┘└┘┴└────┘┴┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴└──────┘┴ ┴
txt └───┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
par └───┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
pid └───┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
209 { apply filter.mem_sets_of_superset hd,
id └─────────────────────────┘ └┘
src └────┘└─────────────────────────┘┴
typ └────┘└─────────────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────────────────────────────────┘└─
210 assume n hn,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
211 simp at hn,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ─────────────┘└─
212 simp [hn, (hd' n).1] },
id └┘ └─┘ ┴
src └────┘ └┘ ┴ └───┘
typ └────┘└┘└┘ └─┘┴┴└───┘
doc └────┘ └┘ ┴ └───┘
txt └────┘ └┘ ┴ └───┘
par └────┘ └┘ ┴ └───┘
pid ┴┴ └┘ ┴ └──┘┴
st ────────────────────────┘└┘└
213 { apply tendsto_prod_mk_nhds _ hy,
id └──────────────────┘ └┘
src └────┘└──────────────────┘└─┘
typ └────┘└──────────────────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ──────────────────────────────────┘└─
214 change tendsto (λ (n : ℕ), c n • d' n) at_top (𝓝 0),
id └─────┘ ┴ └┘ └────┘ ┴
src └─────┘└─────┘┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘└────┘┴ ┴└─┘
typ └─────┘└─────┘┴ └────┘ └─┘┴┴ ┴ ┴└┘┴ └┘└────┘┴ ┴└─┘
doc └─────┘└─────┘┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘└────┘┴ ┴└─┘
txt └─────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
par └─────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
pid ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
st ──────────────────────────────────────────────────────┘└─
215 rw tendsto_zero_iff_norm_tendsto_zero,
id └────────────────────────────────┘
src └─┘└────────────────────────────────┘
typ └─┘└────────────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────────────────────────┘└─
216 refine squeeze_zero (λn, norm_nonneg _) (λn, (hd' n).2) _,
id └──────────┘ └─────────┘ └─┘
src └─────┘└──────────┘┴ └─┘└─────────┘└──┘ └─┘ ┴ └────┘
typ └─────┘└──────────┘┴ └─┘└─────────┘└──┘ └─┘ └─┘┴ └────┘
doc └─────┘ ┴ └─┘ └──┘ └─┘ ┴ └────┘
txt └─────┘ ┴ └─┘ └──┘ └─┘ ┴ └────┘
par └─────┘ ┴ └─┘ └──┘ └─┘ ┴ └────┘
pid ┴ ┴ └─┘ └──┘ └─┘ ┴ └────┘
st ────────────────────────────────────────────────────────────┘└─
217 apply tendsto_pow_at_top_nhds_0_of_lt_1; norm_num }
id └───────────────────────────────┘
src └────┘└───────────────────────────────┘ └───────┘
typ └────┘└───────────────────────────────┘ └───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ ┴
st ─────────────────────────────────────────────────────┘└─
218 end
st ──┘
219
220 /-- If a subset of a real vector space contains a segment, then the direction of this
221 segment belongs to the tangent cone at its endpoints. -/
222 lemma mem_tangent_cone_of_segment_subset {s : set G} {x y : G} (h : segment x y ⊆ s) :
id └─┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └─┘ └─────┘ ┴
typ └─┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
223 y - x ∈ tangent_cone_at ℝ s x :=
id ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src ┴ ┴ └─────────────┘ ┴
typ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
224 begin
st └─────
225 let w : ℝ := 2,
id ┴
src └──────┘┴└───┘
typ └──────┘┴└───┘
doc └──────┘ └───┘
txt └──────┘ └───┘
par └──────┘ └───┘
pid └───┘└─┘ └──┘┴
st ───────────────┘└─
226 let c := λn:ℕ, (2:ℝ)^n,
id ┴
src └───────┘ └┘ └┘ └┘ ┴┴
typ └───────┘ └┘ └┘ └┘ ┴┴
doc └───────┘ └┘ └┘ └┘ ┴
txt └───────┘ └┘ └┘ └┘ ┴
par └───────┘ └┘ └┘ └┘ ┴
pid └───┘┴└─┘ └┘ └┘ └┘ ┴
st ───────────────────────┘└─
227 let d := λn:ℕ, (c n)⁻¹ • (y-x),
id ┴ └┘ ┴ ┴┴┴
src └───────┘ └┘ └┘ ┴ ┴└┘┴┴┴ ┴ ┴
typ └───────┘ └┘ └┘ ┴┴ ┴└┘┴┴┴ ┴┴┴┴
doc └───────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
txt └───────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────┘└─
228 refine ⟨c, d, filter.univ_mem_sets' (λn, h _), _, _⟩,
id ┴ ┴ └───────────────────┘ ┴
src └─────┘ └┘ └┘└───────────────────┘┴ └─┘ └────────┘
typ └─────┘ ┴└┘┴└┘└───────────────────┘┴ └─┘┴└────────┘
doc └─────┘ └┘ └┘ ┴ └─┘ └────────┘
txt └─────┘ └┘ └┘ ┴ └─┘ └────────┘
par └─────┘ └┘ └┘ ┴ └─┘ └────────┘
pid ┴ └┘ └┘ ┴ └─┘ └────────┘
st ─────────────────────────────────────────────────────┘└─
229 show x + d n ∈ segment x y,
id ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
src └───┘ ┴┴┴ ┴ ┴┴┴└─────┘┴ ┴
typ └───┘ ┴┴┴┴┴┴┴┴┴└─────┘┴┴┴┴
doc └───┘ ┴ ┴ ┴ ┴ ┴└─────┘┴ ┴
txt └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────
230 { rw segment_eq_image,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└─────────────────┘└─
231 refine ⟨(c n)⁻¹, ⟨_, _⟩, _⟩,
id ┴ ┴
src └─────┘ ┴ ┴ └┘ └───────┘
typ └─────┘ ┴┴┴┴ └┘ └───────┘
doc └─────┘ ┴ ┴ └┘ └───────┘
txt └─────┘ ┴ ┴ └┘ └───────┘
par └─────┘ ┴ ┴ └┘ └───────┘
pid ┴ ┴ ┴ └┘ └───────┘
st ──────────────────────────────┘└─
232 { rw inv_nonneg, apply pow_nonneg, norm_num },
id └────────┘ └────────┘
src └─┘└────────┘ └────┘└────────┘ └───────┘
typ └─┘└────────┘ └────┘└────────┘ └───────┘
doc └─┘ └────┘ └───────┘
txt └─┘ └────┘ └───────┘
par └─┘ └────┘ └───────┘
pid ┴ ┴ ┴
st ─────┘└───────────┘└────────────────┘└─────────┘└┘└
233 { apply inv_le_one, apply one_le_pow_of_one_le, norm_num },
id └────────┘ └──────────────────┘
src └────┘└────────┘ └────┘└──────────────────┘ └───────┘
typ └────┘└────────┘ └────┘└──────────────────┘ └───────┘
doc └────┘ └────┘ └───────┘
txt └────┘ └────┘ └───────┘
par └────┘ └────┘ └───────┘
pid ┴ ┴ ┴
st ─────┘└──────────────┘└──────────────────────────┘└─────────┘└┘└
234 { simp only [d, sub_smul, smul_sub, one_smul], abel } },
id ┴ └──────┘ └──────┘ └──────┘
src └─────────┘ └┘└──────┘└┘└──────┘└┘└──────┘┴ └───┘
typ └─────────┘┴└┘└──────┘└┘└──────┘└┘└──────┘┴ └───┘
doc └─────────┘ └┘ └┘ └┘ ┴ └───┘
txt └─────────┘ └┘ └┘ └┘ ┴ └───┘
par └─────────┘ └┘ └┘ └┘ ┴ └───┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴ ┴
st ────────────────────────────────────────────────┘└─────┘└──┘└
235 show filter.tendsto (λ (n : ℕ), ∥c n∥) filter.at_top filter.at_top,
id └────────────┘ ┴┴ ┴ └───────────┘
src └───┘└────────────┘┴ └────┘ └─┘┴ ┴ ┴└┘ ┴└───────────┘
typ └───┘└────────────┘┴ └────┘ └─┘┴┴┴ ┴└┘ ┴└───────────┘
doc └───┘└────────────┘┴ └────┘ └─┘ ┴ └┘ ┴└───────────┘
txt └───┘ ┴ └────┘ └─┘ ┴ └┘ ┴
par └───┘ ┴ └────┘ └─┘ ┴ └┘ ┴
pid └───┘ ┴ └────┘ └─┘ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────────────┘└─
236 { have : (λ (n : ℕ), ∥c n∥) = c,
id ┴ ┴
src └─────┘ └────┘ └─┘ ┴ └┘┴┴
typ └─────┘ └────┘ └─┘ ┴ └┘┴┴┴
doc └─────┘ └────┘ └─┘ ┴ └┘ ┴
txt └─────┘ └────┘ └─┘ ┴ └┘ ┴
par └─────┘ └────┘ └─┘ ┴ └┘ ┴
pid └───┘└┘ └────┘ └─┘ ┴ └┘ ┴
st ───┘└───────────────────────────┘
237 by { ext n, exact abs_of_nonneg (pow_nonneg (by norm_num) _) },
id └───────────┘ └────────┘
src └───┘ └────┘└───────────┘┴ └────────┘┴ ┴└──────┘└───┘
typ └───┘ └────┘└───────────┘┴ └────────┘┴ ┴└──────┘└───┘
doc └───┘ └────┘ ┴ ┴ ┴└──────┘└───┘
txt └───┘ └────┘ ┴ ┴ ┴└──────┘└───┘
par └───┘ └────┘ ┴ ┴ ┴└──────┘└───┘
pid └┘ ┴ ┴ ┴ └───────────┘┴
st ┴└────┘└───────────────────────────────────┘└───────┘└───┘└┘└
238 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
239 exact tendsto_pow_at_top_at_top_of_gt_1 (by norm_num) },
id └───────────────────────────────┘
src └────┘└───────────────────────────────┘┴ ┴└──────┘└┘
typ └────┘└───────────────────────────────┘┴ ┴└──────┘└┘
doc └────┘ ┴ ┴└──────┘└┘
txt └────┘ ┴ ┴└──────┘└┘
par └────┘ ┴ ┴└──────┘└┘
pid ┴ ┴ └────────┘┴
st ──────────────────────────────────────────────┘└───────┘└┘└┘└
240 show filter.tendsto (λ (n : ℕ), c n • d n) filter.at_top (𝓝 (y - x)),
id └────────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───┘└────────────┘┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘└───────────┘┴ ┴┴ ┴ ┴ └┘
typ └───┘└────────────┘┴ └────┘ └─┘┴┴ ┴ ┴┴┴ └┘└───────────┘┴ ┴┴ ┴┴ ┴┴└┘
doc └───┘└────────────┘┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘└───────────┘┴ ┴┴ ┴ ┴ └┘
txt └───┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └───┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────┘└─
241 { have : (λ (n : ℕ), c n • d n) = (λn, y - x),
id ┴ ┴ ┴ ┴
src └─────┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴
typ └─────┘ └────┘ └─┘┴┴ ┴ ┴┴┴ └┘ ┴ └─┘┴┴ ┴┴┴
doc └─────┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴
txt └─────┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴
par └─────┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴
pid └───┘└┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
242 { ext n,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ─────┘└───┘└─
243 simp only [d, smul_smul],
id ┴ └───────┘
src └─────────┘ └┘└───────┘┴
typ └─────────┘┴└┘└───────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────────────────────────────┘└─
244 rw [mul_inv_cancel, one_smul],
id └────────────┘ └──────┘
src └──┘└────────────┘└┘└──────┘┴
typ └──┘└────────────┘└┘└──────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────────┘└────────┘└──
245 exact pow_ne_zero _ (by norm_num) },
id └─────────┘
src └────┘└─────────┘└─┘ ┴└──────┘└┘
typ └────┘└─────────┘└─┘ ┴└──────┘└┘
doc └────┘ └─┘ ┴└──────┘└┘
txt └────┘ └─┘ ┴└──────┘└┘
par └────┘ └─┘ ┴└──────┘└┘
pid ┴ └─┘ └────────┘┴
st ────────────────────────────┘└───────┘└┘└┘└
246 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
247 apply tendsto_const_nhds }
id └────────────────┘
src └────┘└────────────────┘┴
typ └────┘└────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────┘└─
248 end
st ──┘
249
250 end tangent_cone
251
252 section unique_diff
253 /- This section is devoted to properties of the predicates `unique_diff_within_at` and
254 `unique_diff_on`. -/
255
256 lemma unique_diff_within_at_univ : unique_diff_within_at 𝕜 univ x :=
id └───────────────────┘ ┴ └──┘ ┴
src └───────────────────┘ └──┘
typ └───────────────────┘ ┴ └──┘ ┴
doc └───────────────────┘
257 by { rw [unique_diff_within_at, tangent_cone_univ], simp }
id └───────────────────┘ └───────────────┘
src └──┘└───────────────────┘└┘└───────────────┘┴ └───┘
typ └──┘└───────────────────┘└┘└───────────────┘┴ └───┘
doc └──┘└───────────────────┘└┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st └──────────────────────────┘└─────────────────┘└──────┘└┘
258
259 lemma unique_diff_on_univ : unique_diff_on 𝕜 (univ : set E) :=
id └────────────┘ ┴ └──┘ └─┘ ┴
src └────────────┘ └──┘ └─┘
typ └────────────┘ ┴ └──┘ └─┘ ┴
doc └────────────┘
260 λx hx, unique_diff_within_at_univ
id ┴ └┘ └────────────────────────┘
src └────────────────────────┘
typ ┴ └┘ └────────────────────────┘
261
262 lemma unique_diff_within_at.mono_nhds (h : unique_diff_within_at 𝕜 s x)
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘
263 (st : nhds_within x s ≤ nhds_within x t) :
id └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └─────────┘ └─────────┘
264 unique_diff_within_at 𝕜 t x :=
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘
265 begin
st └─────
266 unfold unique_diff_within_at at *,
src └───────────────────────────────┘
typ └───────────────────────────────┘
doc └───────────────────────────────┘
txt └───────────────────────────────┘
par └───────────────────────────────┘
pid └────────────────────┘└───┘
st ──────────────────────────────────┘└─
267 rw [← univ_subset_iff, ← h.1],
id └─────────────┘ ┴
src └────┘└─────────────┘└──┘ └─┘
typ └────┘└─────────────┘└──┘┴└─┘
doc └────┘ └──┘ └─┘
txt └────┘ └──┘ └─┘
par └────┘ └──┘ └─┘
pid └──┘ └──┘ └─┘
st ──────────────────────┘└───┘└────
268 rw [mem_closure_iff_nhds_within_ne_bot] at h ⊢,
id └────────────────────────────────┘
src └──┘└────────────────────────────────┘└──────┘
typ └──┘└────────────────────────────────┘└──────┘
doc └──┘ └──────┘
txt └──┘ └──────┘
par └──┘ └──────┘
pid └┘ ┴└─────┘
st ───────────────────────────────────────┘┴└─────┘└─
269 exact ⟨closure_mono (submodule.span_mono (tangent_cone_mono_nhds st)),
id └──────────┘ └─────────────────┘ └────────────────────┘
src └────┘ └──────────┘┴ └─────────────────┘┴ └────────────────────┘┴ └───
typ └────┘ └──────────┘┴ └─────────────────┘┴ └────────────────────┘┴ └───
doc └────┘ ┴ ┴ ┴ └───
txt └────┘ ┴ ┴ ┴ └───
par └────┘ ┴ ┴ ┴ └───
pid ┴ ┴ ┴ ┴ └───
st ─────────────────────────────────────────────────────────────────────────
270 lattice.ne_bot_of_le_ne_bot h.2 st⟩
id └─────────────────────────┘ ┴ └┘
src ───┘└─────────────────────────┘┴ └─┘ └┘
typ ───┘└─────────────────────────┘┴┴└─┘└┘└┘
doc ───┘ ┴ └─┘ └┘
txt ───┘ ┴ └─┘ └┘
par ───┘ ┴ └─┘ └┘
pid ───┘ ┴ └─┘ ┴┴
st ───────────────────────────────────────┘
271 end
st └─┘
272
273 lemma unique_diff_within_at.mono (h : unique_diff_within_at 𝕜 s x) (st : s ⊆ t) :
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────────┘
274 unique_diff_within_at 𝕜 t x :=
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘
275 h.mono_nhds $ nhds_within_mono _ st
id ┴└────────┘ └──────────────┘ └┘
src └────────┘ └──────────────┘
typ ┴└────────┘ └──────────────┘ └┘
276
277 lemma unique_diff_within_at_congr (st : nhds_within x s = nhds_within x t) :
id └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └─────────┘ └─────────┘
278 unique_diff_within_at 𝕜 s x ↔ unique_diff_within_at 𝕜 t x :=
id └───────────────────┘ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘ ┴ └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘ └───────────────────┘
279 ⟨λ h, h.mono_nhds $ le_of_eq st, λ h, h.mono_nhds $ le_of_eq st.symm⟩
id ┴ ┴└────────┘ └──────┘ └┘ ┴ ┴└────────┘ └──────┘ └┘└───┘
src └────────┘ └──────┘ └────────┘ └──────┘ └───┘
typ ┴ ┴└────────┘ └──────┘ └┘ ┴ ┴└────────┘ └──────┘ └┘└───┘
280
281 lemma unique_diff_within_at_inter (ht : t ∈ 𝓝 x) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
doc ┴
282 unique_diff_within_at 𝕜 (s ∩ t) x ↔ unique_diff_within_at 𝕜 s x :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘ ┴ ┴ └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘ └───────────────────┘
283 unique_diff_within_at_congr $ (nhds_within_restrict' _ ht).symm
id └─────────────────────────┘ └───────────────────┘ └┘ └──┘
src └─────────────────────────┘ └───────────────────┘ └──┘
typ └─────────────────────────┘ └───────────────────┘ └┘ └──┘
284
285 lemma unique_diff_within_at.inter (hs : unique_diff_within_at 𝕜 s x) (ht : t ∈ 𝓝 x) :
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────────┘ ┴ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────────┘ ┴
286 unique_diff_within_at 𝕜 (s ∩ t) x :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────────┘
287 (unique_diff_within_at_inter ht).2 hs
id └─────────────────────────┘ └┘ ┴ └┘
src └─────────────────────────┘ ┴
typ └─────────────────────────┘ └┘ ┴ └┘
288
289 lemma unique_diff_within_at_inter' (ht : t ∈ nhds_within x s) :
id ┴ ┴ └─────────┘ ┴ ┴
src ┴ └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴
doc └─────────┘
290 unique_diff_within_at 𝕜 (s ∩ t) x ↔ unique_diff_within_at 𝕜 s x :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘ ┴ ┴ └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘ └───────────────────┘
291 unique_diff_within_at_congr $ (nhds_within_restrict'' _ ht).symm
id └─────────────────────────┘ └────────────────────┘ └┘ └──┘
src └─────────────────────────┘ └────────────────────┘ └──┘
typ └─────────────────────────┘ └────────────────────┘ └┘ └──┘
292
293 lemma unique_diff_within_at.inter' (hs : unique_diff_within_at 𝕜 s x) (ht : t ∈ nhds_within x s) :
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └───────────────────┘ ┴ └─────────┘
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └───────────────────┘ └─────────┘
294 unique_diff_within_at 𝕜 (s ∩ t) x :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────────┘
295 (unique_diff_within_at_inter' ht).2 hs
id └──────────────────────────┘ └┘ ┴ └┘
src └──────────────────────────┘ ┴
typ └──────────────────────────┘ └┘ ┴ └┘
296
297 lemma is_open.unique_diff_within_at (hs : is_open s) (xs : x ∈ s) : unique_diff_within_at 𝕜 s x :=
id └─────┘ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
src └─────┘ ┴ └───────────────────┘
typ └─────┘ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
doc └─────┘ └───────────────────┘
298 begin
st └─────
299 have := unique_diff_within_at_univ.inter (mem_nhds_sets hs xs),
id └──────────────────────────────┘ └───────────┘ └┘ └┘
src └──────┘└──────────────────────────────┘┴ └───────────┘┴ ┴ ┴
typ └──────┘└──────────────────────────────┘┴ └───────────┘┴└┘┴└┘┴
doc └──────┘ ┴ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ ┴
pid └───┘└─┘ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────┘└─
300 rwa univ_inter at this
id └────────┘
src └──┘└────────┘└───────┘
typ └──┘└────────┘└───────┘
doc └──┘ └───────┘
txt └──┘ └───────┘
par └──┘ └───────┘
pid ┴ └──────┘┴
st ────────────────────────┘
301 end
st └─┘
302
303 lemma unique_diff_on.inter (hs : unique_diff_on 𝕜 s) (ht : is_open t) : unique_diff_on 𝕜 (s ∩ t) :=
id └────────────┘ ┴ ┴ └─────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
src └────────────┘ └─────┘ └────────────┘ ┴
typ └────────────┘ ┴ ┴ └─────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
doc └────────────┘ └─────┘ └────────────┘
304 λx hx, (hs x hx.1).inter (mem_nhds_sets ht hx.2)
id ┴ └┘ └┘ ┴ └┘┴ └───┘ └───────────┘ └┘ └┘┴
src ┴ └───┘ └───────────┘ ┴
typ ┴ └┘ └┘ ┴ └┘┴ └───┘ └───────────┘ └┘ └┘┴
305
306 lemma is_open.unique_diff_on (hs : is_open s) : unique_diff_on 𝕜 s :=
id └─────┘ ┴ └────────────┘ ┴ ┴
src └─────┘ └────────────┘
typ └─────┘ ┴ └────────────┘ ┴ ┴
doc └─────┘ └────────────┘
307 λx hx, is_open.unique_diff_within_at hs hx
id ┴ └┘ └───────────────────────────┘ └┘ └┘
src └───────────────────────────┘
typ ┴ └┘ └───────────────────────────┘ └┘ └┘
308
309 /-- The product of two sets of unique differentiability at points `x` and `y` has unique
310 differentiability at `(x, y)`. -/
311 lemma unique_diff_within_at.prod {t : set F} {y : F}
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
312 (hs : unique_diff_within_at 𝕜 s x) (ht : unique_diff_within_at 𝕜 t y) :
id └───────────────────┘ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘ └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘ └───────────────────┘
313 unique_diff_within_at 𝕜 (set.prod s t) (x, y) :=
id └───────────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
src └───────────────────┘ └──────┘ ┴
typ └───────────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
doc └───────────────────┘ └──────┘
314 begin
st └─────
315 rw [unique_diff_within_at, ← univ_subset_iff] at ⊢ hs ht,
id └───────────────────┘ └─────────────┘
src └──┘└───────────────────┘└──┘└─────────────┘└──────────┘
typ └──┘└───────────────────┘└──┘└─────────────┘└──────────┘
doc └──┘└───────────────────┘└──┘ └──────────┘
txt └──┘ └──┘ └──────────┘
par └──┘ └──┘ └──────────┘
pid └┘ └──┘ ┴└─────────┘
st ──────────────────────────┘└─────────────────┘┴└─────────┘└─
316 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
317 { assume v _,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───┘└────────┘└─
318 rw metric.mem_closure_iff',
id └─────────────────────┘
src └─┘└─────────────────────┘
typ └─┘└─────────────────────┘
doc └─┘└─────────────────────┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────────┘└─
319 assume ε ε_pos,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ─────────────────┘└─
320 rcases v with ⟨v₁, v₂⟩,
id ┴
src └─────┘ └────────────┘
typ └─────┘┴└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └────────────┘
st ─────────────────────────┘└─
321 rcases metric.mem_closure_iff'.1 (hs.1 (mem_univ v₁)) ε ε_pos with ⟨w₁, w₁_mem, h₁⟩,
id └─────────────────────┘ └┘ └──────┘ └┘ ┴ └───┘
src └─────┘└─────────────────────┘└─┘ └─┘ └──────┘┴ └─┘ ┴ └────────────────────┘
typ └─────┘└─────────────────────┘└─┘ └┘└─┘ └──────┘┴└┘└─┘┴┴└───┘└────────────────────┘
doc └─────┘└─────────────────────┘└─┘ └─┘ ┴ └─┘ ┴ └────────────────────┘
txt └─────┘ └─┘ └─┘ ┴ └─┘ ┴ └────────────────────┘
par └─────┘ └─┘ └─┘ ┴ └─┘ ┴ └────────────────────┘
pid ┴ └─┘ └─┘ ┴ └─┘ ┴ └────────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
322 rcases metric.mem_closure_iff'.1 (ht.1 (mem_univ v₂)) ε ε_pos with ⟨w₂, w₂_mem, h₂⟩,
id └─────────────────────┘ └┘ └──────┘ └┘ ┴ └───┘
src └─────┘└─────────────────────┘└─┘ └─┘ └──────┘┴ └─┘ ┴ └────────────────────┘
typ └─────┘└─────────────────────┘└─┘ └┘└─┘ └──────┘┴└┘└─┘┴┴└───┘└────────────────────┘
doc └─────┘└─────────────────────┘└─┘ └─┘ ┴ └─┘ ┴ └────────────────────┘
txt └─────┘ └─┘ └─┘ ┴ └─┘ ┴ └────────────────────┘
par └─────┘ └─┘ └─┘ ┴ └─┘ ┴ └────────────────────┘
pid ┴ └─┘ └─┘ ┴ └─┘ ┴ └────────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
323 have I₁ : (w₁, (0 : F)) ∈ submodule.span 𝕜 (tangent_cone_at 𝕜 (set.prod s t) (x, y)),
id └┘ ┴ ┴ └────────────┘ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
src └────────┘ └┘ └──┘ └─┘┴┴└────────────┘┴ ┴ └─────────────┘┴ ┴ └──────┘┴ ┴ └┘┴ └┘ └┘
typ └────────┘ └┘└┘ └──┘┴└─┘┴┴└────────────┘┴ ┴ └─────────────┘┴┴┴ └──────┘┴┴┴┴└┘┴┴└┘┴└┘
doc └────────┘ └┘ └──┘ └─┘ ┴└────────────┘┴ ┴ └─────────────┘┴ ┴ └──────┘┴ ┴ └┘ └┘ └┘
txt └────────┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘
par └────────┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘
pid └─────┘└─┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
324 { apply submodule.span_induction w₁_mem,
id └──────────────────────┘ └────┘
src └────┘└──────────────────────┘┴
typ └────┘└──────────────────────┘┴└────┘
doc └────┘└──────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└───────────────────────────────────┘└─
325 { assume w hw,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───────┘└─────────┘└─
326 have : (w, (0 : F)) ∈ (set.prod (tangent_cone_at 𝕜 s x) {(0 : F)}),
id ┴┴ └──────┘ └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘┴ └┘ └──┘ └─┘ ┴ └──────┘┴ └─────────────┘┴ ┴ ┴ └┘┴ └──┘ └─┘
typ └─────┘┴┴└┘ └──┘ └─┘ ┴ └──────┘┴ └─────────────┘┴┴┴┴┴┴└┘┴ └──┘┴└─┘
doc └─────┘ └┘ └──┘ └─┘ ┴ └──────┘┴ └─────────────┘┴ ┴ ┴ └┘ └──┘ └─┘
txt └─────┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └──┘ └─┘
par └─────┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └──┘ └─┘
pid └───┘└┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └──┘ └─┘
st ─────────────────────────────────────────────────────────────────────────┘└─
327 { rw mem_prod,
id └──────┘
src └─┘└──────┘
typ └─┘└──────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────┘└─────────┘└─
328 simp [hw],
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ──────────────────┘└─
329 apply mem_insert },
id └────────┘
src └────┘└────────┘┴
typ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────┘└┘└
330 have : (w, (0 : F)) ∈ tangent_cone_at 𝕜 (set.prod s t) (x, y) :=
id ┴ ┴ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
src └─────┘ └┘ └──┘ └─┘ ┴└─────────────┘┴ ┴ └──────┘┴ ┴ └┘┴ └┘ └────
typ └─────┘ ┴└┘ └──┘┴└─┘ ┴└─────────────┘┴┴┴ └──────┘┴┴┴┴└┘┴┴└┘┴└────
doc └─────┘ └┘ └──┘ └─┘ ┴└─────────────┘┴ ┴ └──────┘┴ ┴ └┘ └┘ └────
txt └─────┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └────
par └─────┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └────
pid └───┘└┘ └┘ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴└───
st ─────────────────────────────────────────────────────────────────────────
331 subset_tangent_cone_prod_left ht.2 this,
id └───────────────────────────┘ └┘ └──┘
src ─────────┘└───────────────────────────┘┴ └─┘
typ ─────────┘└───────────────────────────┘┴└┘└─┘└──┘
doc ─────────┘└───────────────────────────┘┴ └─┘
txt ─────────┘ ┴ └─┘
par ─────────┘ ┴ └─┘
pid ─────────┘ ┴ └─┘
st ────────────────────────────────────────────────┘└─
332 exact submodule.subset_span this },
id └───────────────────┘ └──┘
src └────┘└───────────────────┘┴ ┴
typ └────┘└───────────────────┘┴└──┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────────────┘└┘└
333 { exact submodule.zero_mem _ },
id └────────────────┘
src └────┘└────────────────┘└─┘
typ └────┘└────────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ───────┘└─────────────────────────┘└┘└
334 { assume a b ha hb,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └──────────────┘
st ───────┘└──────────────┘└─
335 have : (a, (0 : F)) + (b, (0 : F)) = (a + b, (0 : F)), by simp,
id ┴ ┴ ┴┴ ┴ ┴
src └─────┘ └┘ └──┘ └─┘┴┴ └┘ └──┘ └─┘┴┴┴ ┴ ┴ └┘ └──┘ └┘ └──┘
typ └─────┘ └┘ └──┘ └─┘┴┴ └┘ └──┘ └─┘┴┴┴┴┴ ┴┴└┘ └──┘┴└┘ └──┘
doc └─────┘ └┘ └──┘ └─┘ ┴ └┘ └──┘ └─┘ ┴ ┴ ┴ └┘ └──┘ └┘ └──┘
txt └─────┘ └┘ └──┘ └─┘ ┴ └┘ └──┘ └─┘ ┴ ┴ ┴ └┘ └──┘ └┘ └──┘
par └─────┘ └┘ └──┘ └─┘ ┴ └┘ └──┘ └─┘ ┴ ┴ ┴ └┘ └──┘ └┘ └──┘
pid └───┘└┘ └┘ └──┘ └─┘ ┴ └┘ └──┘ └─┘ ┴ ┴ ┴ └┘ └──┘ └┘
st ────────────────────────────────────────────────────────────┘ └─
336 rw ← this,
id └──┘
src └───┘
typ └───┘└──┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────────────┘└─
337 exact submodule.add_mem _ ha hb },
id └───────────────┘ └┘ └┘
src └────┘└───────────────┘└─┘ ┴ ┴
typ └────┘└───────────────┘└─┘└┘┴└┘┴
doc └────┘ └─┘ ┴ ┴
txt └────┘ └─┘ ┴ ┴
par └────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────────────────────────┘└┘└
338 { assume c a ha,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ────────────────────┘└─
339 have : c • (0 : F) = (0 : F), by simp,
id ┴ ┴ ┴
src └─────┘ ┴┴┴ └──┘ └┘ ┴ └──┘ ┴ └──┘
typ └─────┘┴┴┴┴ └──┘ └┘ ┴ └──┘┴┴ └──┘
doc └─────┘ ┴ ┴ └──┘ └┘ ┴ └──┘ ┴ └──┘
txt └─────┘ ┴ ┴ └──┘ └┘ ┴ └──┘ ┴ └──┘
par └─────┘ ┴ ┴ └──┘ └┘ ┴ └──┘ ┴ └──┘
pid └───┘└┘ ┴ ┴ └──┘ └┘ ┴ └──┘ ┴
st ───────────────────────────────────┘ └─
340 rw ← this,
id └──┘
src └───┘
typ └───┘└──┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────────────┘└─
341 exact submodule.smul_mem _ _ ha } },
id └────────────────┘ └┘
src └────┘└────────────────┘└───┘ ┴
typ └────┘└────────────────┘└───┘└┘┴
doc └────┘ └───┘ ┴
txt └────┘ └───┘ ┴
par └────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ───────────────────────────────────────┘└──┘└
342 have I₂ : ((0 : E), w₂) ∈ submodule.span 𝕜 (tangent_cone_at 𝕜 (set.prod s t) (x, y)),
id ┴ └┘ └────────────┘ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
src └────────┘ └──┘ └─┘ └┘ ┴└────────────┘┴ ┴ └─────────────┘┴ ┴ └──────┘┴ ┴ └┘┴ └┘ └┘
typ └────────┘ └──┘┴└─┘└┘└┘ ┴└────────────┘┴ ┴ └─────────────┘┴┴┴ └──────┘┴┴┴┴└┘┴┴└┘┴└┘
doc └────────┘ └──┘ └─┘ └┘ ┴└────────────┘┴ ┴ └─────────────┘┴ ┴ └──────┘┴ ┴ └┘ └┘ └┘
txt └────────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘
par └────────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘
pid └─────┘└─┘ └──┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
343 { apply submodule.span_induction w₂_mem,
id └──────────────────────┘ └────┘
src └────┘└──────────────────────┘┴
typ └────┘└──────────────────────┘┴└────┘
doc └────┘└──────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└───────────────────────────────────┘└─
344 { assume w hw,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───────┘└─────────┘└─
345 have : ((0 : E), w) ∈ (set.prod {(0 : E)} (tangent_cone_at 𝕜 t y)),
id ┴ ┴ └──────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────┘┴ └──┘ └─┘ └┘ ┴ └──────┘┴┴ └──┘ └─┘ └─────────────┘┴ ┴ ┴ └┘
typ └─────┘┴ └──┘ └─┘┴└┘ ┴ └──────┘┴┴ └──┘┴└─┘ └─────────────┘┴┴┴┴┴┴└┘
doc └─────┘ └──┘ └─┘ └┘ ┴ └──────┘┴ └──┘ └─┘ └─────────────┘┴ ┴ ┴ └┘
txt └─────┘ └──┘ └─┘ └┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ └┘
par └─────┘ └──┘ └─┘ └┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ └┘
pid └───┘└┘ └──┘ └─┘ └┘ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────┘└─
346 { rw mem_prod,
id └──────┘
src ┴ └──────┘
typ ┴ └──────┘
doc ┴
txt ┴
par ┴
st ────────┘ ┴ └──────┘└─
347 simp [hw],
id └┘
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘┴
doc ┴ ┴ ┴ ┴
txt ┴ ┴ ┴ ┴
par ┴ ┴ ┴ ┴
pid ┴ ┴
st ──────────┘ ┴ ┴ └─┘ └
348 apply mem_insert },
id └────────┘
src └────┘└────────┘┴
typ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────┘┴ ┴
349 have : ((0 : E), w) ∈ tangent_cone_at 𝕜 (set.prod s t) (x, y) :=
id └┘ ┴ ┴ ┴ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
src └┘ ┴ └─────────────┘ └──────┘ ┴
typ └┘ ┴ ┴ ┴ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
doc └┘ ┴ └─────────────┘ └──────┘
st ┴ └┘ ┴ ┴
350 subset_tangent_cone_prod_right hs.2 this,
id └────────────────────────────┘ └┘┴ └──┘
src └────────────────────────────┘ ┴
typ └────────────────────────────┘ └┘┴ └──┘
doc └────────────────────────────┘
st ┴
351 exact submodule.subset_span this },
id └┘ └────────────────┘ └──┘
src └┘ └────────────────┘
typ └┘ └────────────────┘ └──┘
st └┘
352 { exact submodule.zero_mem _ },
id └────────────────┘
src └────────────────┘
typ └────────────────┘
st └┘
353 { assume a b ha hb,
354 have : ((0 : E), a) + ((0 : E), b) = ((0 : E), a + b), by simp,
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
355 rw ← this,
id └──┘
typ └──┘
356 exact submodule.add_mem _ ha hb },
id └─┘ └───────────┘
src └─┘ └───────────┘
typ └─┘ └───────────┘
st └┘
357 { assume c a ha,
358 have : c • (0 : E) = (0 : E), by simp,
id ┴ ┴
typ ┴ ┴
359 rw ← this,
id └──┘
typ └──┘
360 exact submodule.smul_mem _ _ ha } },
id └──┘ └────┘ └──┘
src └──┘ └────┘ └──┘
typ └──┘ └────┘ └──┘
st └──┘
361 have I : (w₁, w₂) ∈ submodule.span 𝕜 (tangent_cone_at 𝕜 (set.prod s t) (x, y)),
id └┘ └┘ └────────────┘ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
src └────────────┘ └─────────────┘ └──────┘ ┴
typ └┘ └┘ └────────────┘ └─────────────┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴
doc └────────────┘ └─────────────┘ └──────┘
362 { have : (w₁, (0 : F)) + ((0 : E), w₂) = (w₁, w₂), by simp,
id ┴ ┴ ┴└┘ └┘
src ┴
typ ┴ ┴ ┴└┘ └┘
363 rw ← this,
id └──┘
typ └──┘
364 exact submodule.add_mem _ I₁ I₂ },
id └─┘ └─┘ └───────┘
src └─┘ └─┘ └───────┘
typ └─┘ └─┘ └───────┘
st └┘
365 refine ⟨(w₁, w₂), I, _⟩,
id └┘ └┘ ┴
typ └┘ └┘ ┴
366 simp [dist, h₁, h₂] },
id └┘ └┘
typ └┘ └┘
st └┘
367 { simp [closure_prod_eq, mem_prod_iff, hs.2, ht.2] }
id └─────────────┘ └──────────┘ └┘ └┘
src └─────────────┘ └──────────┘
typ └─────────────┘ └──────────┘ └┘ └┘
st └─
368 end
st ──┘
369
370 /-- The product of two sets of unique differentiability is a set of unique differentiability. -/
371 lemma unique_diff_on.prod {t : set F} (hs : unique_diff_on 𝕜 s) (ht : unique_diff_on 𝕜 t) :
id └─┘ ┴ └────────────┘ ┴ ┴ └────────────┘ ┴ ┴
src └─┘ └────────────┘ └────────────┘
typ └─┘ ┴ └────────────┘ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘ └────────────┘
372 unique_diff_on 𝕜 (set.prod s t) :=
id └────────────┘ ┴ └──────┘ ┴ ┴
src └────────────┘ └──────┘
typ └────────────┘ ┴ └──────┘ ┴ ┴
doc └────────────┘ └──────┘
373 λ ⟨x, y⟩ h, unique_diff_within_at.prod (hs x h.1) (ht y h.2)
id ┴┴ ┴ ┴ └────────────────────────┘ └┘ ┴┴ └┘ ┴┴
src └────────────────────────┘ ┴ ┴
typ ┴┴ ┴ ┴ └────────────────────────┘ └┘ ┴┴ └┘ ┴┴
doc └────────────────────────┘
374
375 /-- In a real vector space, a convex set with nonempty interior is a set of unique
376 differentiability. -/
377 theorem unique_diff_on_convex {s : set G} (conv : convex s) (hs : (interior s).nonempty) :
id └─┘ ┴ └────┘ ┴ └──────┘ ┴ └──────┘
src └─┘ └────┘ └──────┘ └──────┘
typ └─┘ ┴ └────┘ ┴ └──────┘ ┴ └──────┘
doc └────┘ └──────┘ └──────┘
378 unique_diff_on ℝ s :=
id └────────────┘ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴
doc └────────────┘
379 begin
st └─────
380 assume x xs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
381 have A : ∀v, ∃a∈ tangent_cone_at ℝ s x, ∃b∈ tangent_cone_at ℝ s x, ∃δ>(0:ℝ), δ • v = b-a,
id ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─────────────┘ ┴ ┴ ┴
typ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
st ─┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └┘ ┴ └─────────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
382 { assume v,
383 rcases hs with ⟨y, hy⟩,
384 have ys : y ∈ s := interior_subset hy,
id ┴ ┴ └┘ ┴ ┴
src ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴
385 have : ∃(δ : ℝ), 0<δ ∧ y + δ • v ∈ s,
id ┴ ┴
typ ┴ ┴
386 { by_cases h : ∥v∥ = 0,
id └──────┘ ┴┴
src └──────┘ ┴
typ └──────┘ ┴┴
doc └──────┘
st └──────┘
387 { exact ⟨1, zero_lt_one, by simp [(norm_eq_zero _).1 h, ys]⟩ },
id └─────────┘ └──────────┘ ┴ ┴ └┘
src └─────────┘ └──────────┘ ┴
typ └─────────┘ └──────────┘ ┴ ┴ └┘
st └┘
388 { rcases mem_interior.1 hy with ⟨u, us, u_open, yu⟩,
id └──────────┘┴ └┘
src └──────────┘┴
typ └──────────┘┴ └┘
389 rcases metric.is_open_iff.1 u_open y yu with ⟨ε, εpos, hε⟩,
id └────────────────┘┴ └────┘ ┴ └┘
src └────────────────┘┴
typ └────────────────┘┴ └────┘ ┴ └┘
390 let δ := (ε/2) / ∥v∥,
id ┴┴ ┴
src ┴
typ ┴┴ ┴
391 have δpos : 0 < δ := div_pos (half_pos εpos) (lt_of_le_of_ne (norm_nonneg _) (ne.symm h)),
id ┴
typ ┴
392 have : y + δ • v ∈ s,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
393 { apply us (hε _),
394 rw [metric.mem_ball, dist_eq_norm],
395 calc ∥(y + δ • v) - y ∥ = ∥δ • v∥ : by {congr' 1, abel }
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
396 ... = ∥δ∥ * ∥v∥ : norm_smul _ _
397 ... = δ * ∥v∥ : by simp only [norm, abs_of_nonneg (le_of_lt δpos)]
398 ... = ε /2 : div_mul_cancel _ h
399 ... < ε : half_lt_self εpos },
id ┴
typ ┴
st └┘
400 exact ⟨δ, δpos, this⟩ } },
id ┴
typ ┴
st └──┘
401 rcases this with ⟨δ, δpos, hδ⟩,
402 refine ⟨y-x, _, (y + δ • v) - x, _, δ, δpos, by abel⟩,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
403 exact mem_tangent_cone_of_segment_subset (conv.segment_subset xs ys),
404 exact mem_tangent_cone_of_segment_subset (conv.segment_subset xs hδ) },
st └┘
405 have B : ∀v:G, v ∈ submodule.span ℝ (tangent_cone_at ℝ s x),
id ┴ ┴ ┴
typ ┴ ┴ ┴
406 { assume v,
407 rcases A v with ⟨a, ha, b, hb, δ, hδ, h⟩,
id ┴
typ ┴
408 have : v = δ⁻¹ • (b - a),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
409 by { rw [← h, smul_smul, inv_mul_cancel, one_smul], exact (ne_of_gt hδ) },
st └┘
410 rw this,
411 exact submodule.smul_mem _ _
412 (submodule.sub_mem _ (submodule.subset_span hb) (submodule.subset_span ha)) },
st └┘
413 refine ⟨univ_subset_iff.1 (λv hv, subset_closure (B v)), subset_closure xs⟩
id ┴
typ ┴
414 end
st └─┘
415
416 /-- The real interval `[0, 1]` is a set of unique differentiability. -/
417 lemma unique_diff_on_Icc_zero_one : unique_diff_on ℝ (Icc (0:ℝ) 1) :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
418 begin
419 apply unique_diff_on_convex (convex_Icc 0 1),
420 have : (1/(2:ℝ)) ∈ interior (Icc (0:ℝ) 1) :=
id ┴ ┴ └──────┘ └─┘
src ┴ ┴ └──────┘ └─┘
typ ┴ ┴ └──────┘ └─┘
doc └──────┘ └─┘
st ┴ └┘ ┴ ┴ └──────┘ └──┘ ┴ ┴
421 mem_interior.2 ⟨Ioo (0:ℝ) 1, Ioo_subset_Icc_self, is_open_Ioo, by norm_num, by norm_num⟩,
id └──────────┘ └─┘ └─────────────────┘ └─────────┘
src └──────────┘ └─┘ └─────────────────┘ └─────────┘
typ └──────────┘ └─┘ └─────────────────┘ └─────────┘
doc └─┘
st └──────────┘ └──┘ ┴ ┴ └─────────────────┘ └─────────┘ └┘ └──────┘
422 exact ⟨_, this⟩
id └──┘
typ └──┘
423 end
st └─┘
424
425 end unique_diff